User blog:P進大好きbot/A Generic System Analogous to Kleene's O
This is an English translation of my Japanese blog post submitted to a Japanese event. I construct variants of non-recursive ordinal notation Kleene's \(\mathcal{O}\). I denote by \(X\) the set of partial maps \(\mathbb{N} \to \mathbb{N}\). Let \(F\) be a map \(\mathbb{N} \setminus \{0\} \to X\) whose image contains all total constant maps. For example, one can explicitly construct such an \(F\) by modifying enumerations of codes of primitive recursive functions, Turing machines, or other specific computation models. In this blog post, given such an \(F\), I construct an explicit notation \(T_F\) of ordinals, which is not an ordinal notation defined in arithmetic but is a notation with a correspondence to ordinals defined in set theory. = Fundamental Sequence = I denote by \(\mathcal{P}(\mathbb{N})\) the set of subsets of \(\mathbb{N}\). I define a map \begin{eqnarray*} \mathcal{G}_F \colon \omega_1 & \to & \mathcal{P}(\mathbb{N}) \\ \alpha & \mapsto & \mathcal{G}_F(\alpha) \end{eqnarray*} in the following transfinitely inductive way: # If \(\textrm{cof}(\alpha) = 0\), then \(\mathcal{G}_F(\alpha) := \{0\}\). # If \(\textrm{cof}(\alpha) = 1\), then \(\mathcal{G}_F(\alpha)\) is the set of all \(a \in \mathbb{N} \setminus \{0\}\) satisfying the following: ## \(\textrm{dom}(F(a)) = \mathbb{N}\). ## \(a \notin \bigcup_{\beta \in \alpha} \mathcal{G}_F(\beta)\). ## There exists an \(m \in \mathcal{G}_F(\max \alpha)\) such that every \(n \in \mathbb{N}\) satisfies \(F(a)(n) = m\). # If \(\textrm{cof}(\alpha) = \omega\), then \(\mathcal{G}_F(\alpha)\) is the set of all \(a \in \mathbb{N} \setminus \{0\}\) satisfying the following: ## \(\textrm{dom}(F(a)) = \mathbb{N}\). ## \(a \notin \bigcup_{\beta \in \alpha} \mathcal{G}_F(\beta)\). ## For any \(n \in \mathbb{N}\), \(F(a)(n) \in \bigcup_{\beta \in \alpha} \mathcal{G}_F(\beta)\). ## For any \(n \in \mathbb{N}\), there exist \(\beta,\gamma \in \alpha\) such that \(F(a)(n) \in \mathcal{G}_F(\beta)\), \(F(a)(n+1) \in \gamma\), and \(\beta \in \gamma\). I put \(T_F := \bigcup_{\alpha \in \omega_1} \mathcal{G}_F(\alpha) \in \mathcal{P}(\mathbb{N})\). For each \(a \in T_F\), I denote by \(o_F(a)\) the unique \(\alpha \in \omega_1\) satisfying \(a \in \mathcal{G}_F(\alpha)\). I define a map \begin{eqnarray*} [ \ ]_F \colon T_F \times \mathbb{N} & \to & \mathbb{N} \\ (a,n) & \mapsto & an_F \end{eqnarray*} in the following way: # If \(\textrm{cof}(o_F(a)) = 0\), then \(an_F := 0\). # If \(\textrm{cof}(o_F(a)) = 1\), then \(an_F := F(a)(0)\). # If \(\textrm{cof}(o_F(a)) = \omega\), then \(an_F := F(a)(n)\). The map \([ \ ]_F\) gives a system of fundamental sequences compatible with \(o_F\). In other words, \(\textrm{cof}(o_F(a)) = 1\) implies \(o_F(a0) = \max o_F(a)\), and \(\textrm{cof}(o_F(a)) = \omega\) implies that \(o_F(an)\) forms a fundamental sequence of \(o_F(a)\). As a result, \(T_F\) forms a (generally uncomputable) notation equipped with a correspondence \(o_F\) to ordinals and a system \([ \ ]_F\) of fundamental sequences compatible with it. Fast-Growing Function I define a map \begin{eqnarray*} f_F \colon T_F \times \mathbb{N} & \to & \mathbb{N} \\ (a,n) & \mapsto & f_{F,a}(n) \end{eqnarray*} in the following transfinitely inductive way: # If \(\textrm{cof}(o_F(a)) = 0\), then \(f_{F,a}(n) := n+1\). # If \(\textrm{cof}(o_F(a)) \neq 0\), then \(f_{F,a}(n) := \sum_{m=0}^{n} f_{F,am}^n(n)\). By the well-foundedness of ordinals and the compatibility of \([ \ ]_F\) and \(o_F\), \(f_F\) is actually defined on \(T_F \times \mathbb{N}\). I define a map \begin{eqnarray*} \textrm{enum}_F \colon \mathbb{N} & \to & T_F \\ n & \mapsto & \textrm{enum}(n) \end{eqnarray*} in the following inductive way: # If \(n = 0\), then \(\textrm{enum}(n) := 0\). # If \(n \neq 0\), then \(\textrm{enum}(n) := \min \{a \in T_F \mid a > \textrm{enum}(n-1)\}\). In other words, \(\textrm{enum}_F\) is the enumeration function of \(T_F\). I define a map \begin{eqnarray*} \textrm{Lim}_F \colon \mathbb{N} & \to & \mathbb{N} \\ n & \mapsto & \textrm{Lim}_F(n) \end{eqnarray*} in the following way: # If \(n = 0\), then \(\textrm{Lim}_F(n) := f_{F,\textrm{enum}(n)}(n)\). # If \(n \neq 0\), then \(\textrm{Lim}_F(n) := f_{F,\textrm{enum}(n)}^{\textrm{Lim}_F(n-1)}(n)\). As a result, I have uniquely constructed a fast-growing function \(\textrm{Lim}_F\) from an \(F\). In particular, defining \(F\) as the maps \(\mathbb{N} \setminus \{0\} \to X\) given by modifying enumerations of codes of primitive recursive functions or Turing machines, I obtain explicit large functions. Conjecturally, the large function associated to an enumeration of codes of Turing machines is approximated by \(f_{\omega_1^{\textrm{CK}}}\) with respect to Kleene's \(\mathcal{O}\). How about the large function associated to an enumeration of codes of primitive recursive functions? Category:Blog posts